@inproceedings{DBLP:conf/ifm/LucanuR13,
  author    = {Dorel Lucanu and
               Vlad Rusu},
  title     = {Program Equivalence by Circular Reasoning},
  booktitle = {IFM},
  year      = {2013},
  pages     = {362-377},
  ee        = {http://dx.doi.org/10.1007/978-3-642-38613-8_25},
  crossref  = {DBLP:conf/ifm/2013},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ifm/2013,
  editor    = {Einar Broch Johnsen and
               Luigia Petre},
  title     = {Integrated Formal Methods, 10th International Conference,
               IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings},
  booktitle = {IFM},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7940},
  year      = {2013},
  isbn      = {978-3-642-38612-1, 978-3-642-38613-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-38613-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{coq,
title = {The {Coq} Proof Assistant Reference manual, \url{http://coq.inria.fr/refman/}}
}
@inproceedings{rosu-lucanu-2009-calco,
  author = 	 {Grigore Ro\c{s}u and Dorel Lucanu},
  title = 	 {Circular Coinduction -- A Proof Theoretical Foundation},
  booktitle = {CALCO 2009},
  year      = {2009},
  series    = {LNCS},
  volume    = {5728},
  pages     = {127--144},
  publisher = {Springer},
}

@article{lgg,
  author    = {Gordon D. Plotkin},
  title     = {A note on inductive generalization},
  journal   = {Machine Intelligence},
  volume    = {5},
  year      = {1970},
  pages     = {153-163},
  }


@techreport{rosu-stefanescu-2012-tr-g, 
  author      = {G.~Ro{\c s}u and A.~{\c S}tef{\u a}nescu}, 
  institution = {University of Illinois}, 
  title       = {Checking Reachability using Matching Logic}, 
  number      = {http://hdl.handle.net/2142/33771},
  month       = {August},
  year        = {2012},
}

@inproceedings{rosu-stefanescu-2012-icalp,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {Towards a Unified Theory of Operational and Axiomatic Semantics},
  booktitle = {Proceedings of the 39th International Colloquium on Automata, Languages and Programming (ICALP'12)},
  pages     = {351-363},
  volume    = {7392},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2012},
}


@techreport{arusoaie:hal-00766220,
    hal_id = {hal-00766220},
    url = {http://hal.inria.fr/hal-00766220},
    title = {{A Generic Approach to Symbolic Execution}},
    author = {Arusoaie, Andrei and Lucanu, Dorel and Rusu, Vlad},
    abstract = {{We propose a generic, language-independent symbolic execution approach for languages endowed with a formal operational semantics based on term rewriting. Starting from the definition of a language $\cal L$, a new definition ${\cal L}^{\it sym}$ is automatically generated, which has the same syntax, but whose semantics extends ${\cal L}$'s data domains with symbolic values and adapts the semantical rules of $\cal L$ to deal with the new domains. Then, the symbolic execution of ${\cal L}$ programs is the concrete execution of the corresponding ${\cal L}^{\it sym}$ programs, i.e., the application of the rewrite rules in the semantics of ${\cal L}^{\it sym}$. We prove that the symbolic execution thus defined has the adequate properties normally expected from it, and illustrate the approach on a simple imperative language defined in the $\mathbb{\K}$ framework. A prototype symbolic execution engine also written in $\mathbb{\K}$ is presented.}},
    keywords = {Symbolic Execution, Term Rewriting, $\mathbb{\K}$ framework},
    language = {Anglais},
    affiliation = {Department of Compter Science , Department of Computer Science , DART - INRIA Lille - Nord Europe},
    pages = {21},
    type = {Research report},
    institution = {INRIA},
    number = {RR-8189},
    year = {2012},
    month = Dec,
    pdf = {http://hal.inria.fr/hal-00766220/PDF/symbexec-techreport.pdf},
}



@book{Baader:1998:TR:280474,
  author    = {Franz Baader and
               Tobias Nipkow},
  title     = {Term rewriting and all that},
  publisher = {Cambridge University Press},
  year      = {1998},
  isbn      = {978-0-521-45520-6},
  pages     = {I-XII, 1-301},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  address = {New York, NY, USA},
} 


@article{DBLP:journals/iandc/LynchV95,
  author    = {Nancy A. Lynch and
               Frits W. Vaandrager},
  title     = {Forward and Backward Simulations: {I.~Untimed} Systems},
  journal   = {Inf. Comput.},
  volume    = {121},
  number    = {2},
  year      = {1995},
  pages     = {214-233},
  ee        = {http://dx.doi.org/10.1006/inco.1995.1134},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/rta/Meseguer00,
  author    = {Jos{\'e} Meseguer},
  title     = {Rewriting Logic and {Maude}: Concepts and Applications},
  booktitle = {RTA},
  year      = {2000},
  pages     = {1-26},
  ee        = {http://dx.doi.org/10.1007/10721975_1},
  crossref  = {DBLP:conf/rta/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2000,
  editor    = {Leo Bachmair},
  title     = {Rewriting Techniques and Applications, 11th International
               Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings},
  booktitle = {RTA},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1833},
  year      = {2000},
  isbn      = {3-540-67778-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/iandc/SerbanutaRM09,
  author    = {Traian-Florin {\c S}erb{\u a}nu{\c t}{\u a} and
               Grigore Ro{\c s}u and
               Jos{\'e} Meseguer},
  title     = {A rewriting logic approach to operational semantics},
  journal   = {Inf. Comput.},
  volume    = {207},
  number    = {2},
  year      = {2009},
  pages     = {305-340},
  ee        = {http://dx.doi.org/10.1016/j.ic.2008.03.026},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/entcs/EscobarMS09,
  author    = {Santiago Escobar and
               Jos{\'e} Meseguer and
               Ralf Sasse},
  title     = {Variant Narrowing and Equational Unification},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {238},
  number    = {3},
  year      = {2009},
  pages     = {103-119},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.05.015},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/lisp/MeseguerT07,
  author    = {Jos{\'e} Meseguer and
               Prasanna Thati},
  title     = {Symbolic reachability analysis using narrowing and its application
               to verification of cryptographic protocols},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {20},
  number    = {1-2},
  year      = {2007},
  pages     = {123-160},
  ee        = {http://dx.doi.org/10.1007/s10990-007-9000-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{rosu-stefanescu-2012-oopsla,
  author    = {Grigore Ro{\c s}u and
               Andrei {\c S}tef{\u a}nescu},
  title     = {Checking reachability using matching logic},
  booktitle = {OOPSLA},
  year      = {2012},
  pages     = {555-574},
  ee        = {http://doi.acm.org/10.1145/2384616.2384656},
  crossref  = {DBLP:conf/oopsla/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de},
note = {Also available as technical report \url{http://hdl.handle.net/2142/33771}.}
}
@proceedings{DBLP:conf/oopsla/2012,
  editor    = {Gary T. Leavens and
               Matthew B. Dwyer},
  title     = {Proceedings of the 27th Annual {ACM SIGPLAN} Conference on
               Object-Oriented Programming, Systems, Languages, and Applications,
               {OOPSLA} 2012, part of {SPLASH} 2012, Tucson, AZ, USA, October
               21-25, 2012},
  booktitle = {OOPSLA},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1561-6},
  ee        = {http://dl.acm.org/citation.cfm?id=2384616},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Misc{RL,
  author = 	 {Grigore Ro\c{s}u and Dorel Lucanu},
  title = 	 {Circular Behavioural Reasoning},
  howpublished = {Draft Document},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{rosu-stefanescu-2011-nier-icse,
title = {Matching {Logic}: {A} {New} {Program} {Verification} {Approach} ({NIER} {Track})},
author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu},
booktitle = {ICSE'11: Proceedings of the 30th International Conference on Software Engineering},
year = {2011},
pages = {868--871},
ee = {http://doi.acm.org/10.1145/1985793.1985928},
doi = {doi:10.1145/1985793.1985928},
publisher = {ACM},
isbn = {978-1-4503-0445-0},
}

@inproceedings{CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  publisher = {ACM},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995}
}

@article{King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Plotkin70,
  author = {Plotkin, Gordon D.},
  journal = {Machine Intelligence},
  pages = {153--163},
  title = {A Note on Inductive Generalization},
  volume = 5,
  year = 1970
}

@article{AlpuenteEMO09,
  author    = {Mar\'{\i}a Alpuente and
               Santiago Escobar and
               Jos{\'e} Meseguer and
               Pedro Ojeda},
  title     = {Order-Sorted Generalization},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {246},
  year      = {2009},
  pages     = {27-38},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.07.013}
}


@article{DBLP:journals/cacm/King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icse/CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u }areanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995},
  crossref  = {DBLP:conf/icse/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icse/2011,
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  title     = {Proceedings of the 33rd International Conference on Software
               Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May
               21-28, 2011},
  booktitle = {ICSE},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0445-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/sttt/PasareanuV09,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {A survey of new trends in symbolic execution for software
               testing and analysis},
  journal   = {STTT},
  volume    = {11},
  number    = {4},
  year      = {2009},
  pages     = {339-353},
  ee        = {http://dx.doi.org/10.1007/s10009-009-0118-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/kbse/PasareanuR10,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Neha Rungta},
  title     = {Symbolic PathFinder: symbolic execution of {Java} bytecode},
  booktitle = {ASE},
  year      = {2010},
  pages     = {179-180},
  ee        = {http://doi.acm.org/10.1145/1858996.1859035}
}

@inproceedings{DBLP:conf/issta/VisserPK04,
  author    = {Willem Visser and
               Corina S. P{\u a}s{\u a}reanu and
               Sarfraz Khurshid},
  title     = {Test input generation with {J}ava {PathFinder}},
  booktitle = {ISSTA},
  year      = {2004},
  pages     = {97-107},
  ee        = {http://doi.acm.org/10.1145/1007512.1007526},
  crossref  = {DBLP:conf/issta/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2004,
  editor    = {George S. Avrunin and
               Gregg Rothermel},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2004, {B}oston, {M}assachusetts,
               {USA}, July 11-14, 2004},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2004},
  isbn      = {1-58113-820-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@proceedings{DBLP:conf/kbse/2010,
  editor    = {Charles Pecheur and
               Jamie Andrews and
               Elisabetta Di Nitto},
  title     = {ASE 2010, 25th IEEE/ACM International Conference on Automated
               Software Engineering,  Antwerp, Belgium, September 20-24,
               2010},
  booktitle = {ASE},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-4503-0116-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@MISC{pex,
   author  = {{Pex}: Automated exploratory testing for {.NET}},
   url         ={\texttt{http://research.microsoft.com/en-us/projects/pex}},
   note     ={\\ \texttt{http://research.microsoft.com/en-us/projects/pex}}
   }
   
 @inproceedings{HalleuxT08,
  author    = {Jonathan de Halleux and
               Nikolai Tillmann},
  title     = {Parameterized Unit Testing with {Pex}},
  booktitle = {TAP},
  year      = {2008},
  pages     = {171-181},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4966},
  ee        = {http://dx.doi.org/10.1007/978-3-540-79124-9_12},
  }

   

@inproceedings{Godefroid:2005:DDA:1065010.1065036,
  author    = {Patrice Godefroid and
               Nils Klarlund and
               Koushik Sen},
  title     = {{DART}: directed automated random testing},
  booktitle = {PLDI},
  year      = {2005},
  pages     = {213-223},
  ee        = {http://doi.acm.org/10.1145/1065010.1065036},
  crossref  = {DBLP:conf/pldi/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/pldi/2005,
  editor    = {Vivek Sarkar and
               Mary W. Hall},
  title     = {Proceedings of the {ACM SIGPLAN} 2005 Conference on Programming
               Language Design and Implementation, Chicago, IL, USA, June
               12-15, 2005},
  booktitle = {PLDI},
  publisher = {ACM},
  year      = {2005},
  isbn      = {1-59593-056-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Sen:2005:CCU:1081706.1081750,
 author = {Sen, Koushik and Marinov, Darko and Agha, Gul},
 title = {{CUTE}: a concolic unit testing engine for {C}},
 booktitle = {Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering},
 series = {ESEC/FSE-13},
 year = {2005},
 isbn = {1-59593-014-0},
 location = {Lisbon, Portugal},
 pages = {263--272},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1081706.1081750},
 doi = {10.1145/1081706.1081750},
 acmid = {1081750},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concolic testing, data structure testing, explicit path model-checking, random testing, testing {C} programs, unit testing},
}

@inproceedings{DBLP:conf/aplas/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Symbolic Execution with Separation Logic},
  booktitle = {APLAS},
  year      = {2005},
  pages     = {52-68},
  ee        = {http://dx.doi.org/10.1007/11575467_5},
  crossref  = {DBLP:conf/aplas/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aplas/2005,
  editor    = {Kwangkeun Yi},
  title     = {Programming Languages and Systems, Third Asian Symposium,
               APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings},
  booktitle = {APLAS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3780},
  year      = {2005},
  isbn      = {3-540-29735-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Cadar06exe:automatically,
  author    = {Cristian Cadar and
               Vijay Ganesh and
               Peter M. Pawlowski and
               David L. Dill and
               Dawson R. Engler},
  title     = {{EXE}: automatically generating inputs of death},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {2006},
  pages     = {322-335},
  ee        = {http://doi.acm.org/10.1145/1180405.1180445},
  crossref  = {DBLP:conf/ccs/2006usa},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}
@proceedings{DBLP:conf/ccs/2006usa,
  editor    = {Ari Juels and
               Rebecca N. Wright and
               Sabrina De Capitani di Vimercati},
  title     = {Proceedings of the 13th ACM Conference on Computer and Communications
               Security, CCS 2006, Alexandria, VA, USA, Ioctober 30 - November
               3, 2006},
  booktitle = {ACM Conference on Computer and Communications Security},
  publisher = {ACM},
  year      = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}

@article{rosu-serbanuta-2010-jlap,
  title={An Overview of the {K} Semantic Framework},
  author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
  journal={Journal of Logic and Algebraic Programming},
  volume={79},
  number={6},
  pages={397--434},
  year={2010},
  ee={http://dx.doi.org/10.1016/j.jlap.2010.03.012},
  doi={10.1016/j.jlap.2010.03.012},
}


@inproceedings{klover,
  author    = {Guodong Li and
               Indradeep Ghosh and
               Sreeranga P. Rajan},
  title     = {{KLOVER}: A Symbolic Execution and Automatic Test Generation
               Tool for {C++} Programs},
  booktitle = {CAV},
  year      = {2011},
  pages     = {609-615},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1_49},
  crossref  = {DBLP:conf/cav/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2011,
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {Computer Aided Verification - 23rd International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6806},
  year      = {2011},
  isbn      = {978-3-642-22109-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Khurshid03generalizedsymbolic,
  author    = {Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Generalized Symbolic Execution for Model Checking and Testing},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems, 9th International Conference, {TACAS}'03},
  year      = {2003},
  pages     = {553-568},
  ee        = {http://dx.doi.org/10.1007/3-540-36577-X_40},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2003,
  editor    = {Hubert Garavel and
               John Hatcliff},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 9th International Conference, {TACAS} 2003, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, {ETAPS} 2003, {Warsaw}, {Poland}, {April}
               7-11, 2003, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2619},
  year      = {2003},
  isbn      = {3-540-00898-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{Dillon:1990:VGS:78617.78622,
 author = {Dillon, Laura K.},
 title = {Verifying General Safety Properties of {Ada} Tasking Programs},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {January 1990},
 volume = {16},
 number = {1},
 month = jan,
 year = {1990},
 issn = {0098-5589},
 pages = {51--63},
 numpages = {13},
 url = {http://dx.doi.org/10.1109/32.44363},
 doi = {10.1109/32.44363},
 acmid = {78622},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 keywords = {Ada, Ada tasking programs, automating partial correctness proofs, concurrent programs, deadlock, isolation approach, multiprocessing programs, mutual exclusion, program verification., safety properties verification, symbolic execution},
}


@inproceedings{Siegel:2006:UMC:1146238.1146256,
  author    = {Stephen F. Siegel and
               Anastasia Mironova and
               George S. Avrunin and
               Lori A. Clarke},
  title     = {Using model checking with symbolic execution to verify parallel
               numerical programs},
  booktitle = {ISSTA},
  year      = {2006},
  pages     = {157-168},
  ee        = {http://doi.acm.org/10.1145/1146238.1146256},
  crossref  = {DBLP:conf/issta/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2006,
  editor    = {Lori L. Pollock and
               Mauro Pezz{\`e}},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2006, {Portland}, {Maine},
               {USA}, {J}uly 17-20, 2006},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2006},
  isbn      = {1-59593-263-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Staats:2010:PSE:1831708.1831732,
  author    = {Matt Staats and
               Corina S. P{\u a}s{\u a}reanu},
  title     = {Parallel symbolic execution for structural test generation},
  booktitle = {ISSTA},
  year      = {2010},
  pages     = {183-194},
  ee        = {http://doi.acm.org/10.1145/1831708.1831732},
  crossref  = {DBLP:conf/issta/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2010,
  editor    = {Paolo Tonella and
               Alessandro Orso},
  title     = {Proceedings of the Nineteenth International Symposium on
               Software Testing and Analysis, {ISSTA} 2010, {T}rento, {I}taly,
               {J}uly 12-16, 2010},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-60558-823-0},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}


@inproceedings{Pasareanu04verificationof ,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Verification of {J}ava Programs Using Symbolic Execution and
               Invariant Generation},
  booktitle = {SPIN},
  year      = {2004},
  pages     = {164-181},
  ee        = {http://dx.doi.org/10.1007/978-3-540-24732-6_13},
  crossref  = {DBLP:conf/spin/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/spin/2004,
  editor    = {Susanne Graf and
               Laurent Mounier},
  title     = {Model Checking Software, 11th International {SPIN} Workshop,
               {Barcelona}, {Spain}, {April} 1-3, 2004, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2989},
  year      = {2004},
  isbn      = {3-540-21314-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{Lee2003523,
title = {Generating test sequences using symbolic execution for event-driven real-time systems},
journal = "Microprocessors and Microsystems",
volume = "27",
number = "10",
pages = "523 - 531",
year = "2003",
note = "",
issn = "0141-9331",
doi = "10.1016/S0141-9331(03)00102-9",
url = "http://www.sciencedirect.com/science/article/pii/S0141933103001029",
author = "Nam Hee Lee and Sung Deok Cha",
keywords = "Real-time system testing",
keywords = "Symbolic execution",
keywords = "Modechart"
}


@inproceedings{schmitt07,
  author    = {Peter H. Schmitt and
               Benjamin Wei{\ss}},
  title     = {Inferring Invariants by Symbolic Execution},
  booktitle = {VERIFY},
  year      = {2007},
  ee        = {http://ceur-ws.org/Vol-259/paper16.pdf},
  crossref  = {DBLP:conf/cade/2007verify},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2007verify,
  editor    = {Bernhard Beckert},
  title     = {Proceedings of 4th International Verification Workshop in
               connection with {CADE}-21, {B}remen, {G}ermany, July 15-16, 2007},
  booktitle = {VERIFY},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {259},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{lucanu:hal-00744374,
    hal_id = {hal-00744374},
    url = {http://hal.inria.fr/hal-00744374},
    title = {Program Equivalence by Circular Reasoning},
    author = {Lucanu, Dorel and Rusu, Vlad},
    abstract = {We propose a deductive system for automatically proving the equivalence of programs written in deterministic languages that have a formal, term-rewriting based operational semantics. Symbolic programs (i.e., programs in which some statements or expressions are symbolic variables) can also be proved equivalent using the proposed approach. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that the deductive system is suitable for proving equivalence both for terminating and non-terminating programs. We also report on a prototype implementation of the proposed system in the $\mathbb{K}$ framework},
    language = {Anglais},
    affiliation = {Department of Computer Science , DART - INRIA Lille - Nord Europe},
    pages = {26},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-8116},
    year = {2012},
    month = Oct,
    pdf = {http://hal.inria.fr/hal-00744374/PDF/RR-8116.pdf},
}

@MISC{imponline,
   author = {Symbolic \IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}

@book{Apt,
 author = {Apt, Krzysztof R. and de Boer, Frank and Olderog, Ernst-R{\"u}diger},
 title = {Verification of Sequential and Concurrent Programs},
 year = {2009},
 isbn = {184882744X, 9781848827448},
 edition = {3rd},
 publisher = {Springer Verlag},
} 

@inproceedings{ArusoaieLR2013SLE,
    author    = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu},
    title     = {A Generic Framework for Symbolic Execution},
    booktitle = {6th International Conference on Software Language Engineering},
    publisher = {Springer Verlag},
    volume   = {8225},
    series   = {LNCS},
    pages    = {281-301},
    year      = {2013},
   note = {Also available as a technical report at \url{http://hal.inria.fr/hal-00766220/}.}
}

@inproceedings{meredith-hills-rosu-2007-scheme,
author = {Patrick Meredith, Mark Hills, Grigore Ro\c{s}u},
title = "{An Executable Rewriting Logic Semantics of K-Scheme}",
year = {2007},
editor = {Danny Dube},
booktitle = {Proceedings of the 2007 Workshop on Scheme and Functional Programming (SCHEME'07), Technical Report DIUL-RT-0701},
publisher = {Laval University},
pages = {91--103}
}

@inproceedings{meredith-katelman-meseguer-rosu-2010-memocode,
author={Patrick O'Neil Meredith and Michael Katelman and Jos{\'e} Meseguer and Grigore Ro\c{s}u},
title={A Formal Executable Semantics of {V}erilog},
booktitle={Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'10)},
year={2010},
publisher={IEEE},
pages={179-188},
doi={doi:10.1109/MEMCOD.2010.555863}
}

@InProceedings{ellison-rosu-2012-popl,
author = "Chucky Ellison and Grigore Ro{\c s}u",
title = "An Executable Formal Semantics of {C} with Applications",
booktitle = "Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12)",
year = "2012",
pages = "533-544",
publisher = "ACM",
doi = "10.1145/2103656.2103719"
}

@mastersthesis{guth-2013-thesis,
    author = "Guth, Dwight",
    school = "University of Illinois at Urbana-Champaign",
    month = "July",
    year = "2013",
    title = "A Formal Semantics of {Python} 3.3"
}

@misc{java,
    author = {Denis Bogd\u{a}na\c{s}},
    title     = {{J}ava semantics in $\mathbb{K}$},
    howpublished = {\url{https://github.com/kframework/java-semantics}},
}

@misc{k,
    title     = {The $\mathbb{K}$ tool},
    howpublished =  {\url{https://github.com/kframework/k}},
}

@misc{ocaml,
    author = {David Laz\u{a}r},
    title     = {{OC}aml semantics in  $\mathbb{K}$},
    howpublished =  {\url{https://github.com/kframework/ocaml-semantics}},
}

@inproceedings{DBLP:conf/tacas/MouraB08,
  author = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title = { {Z3}: An Efficient {SMT} Solver},
  year = {2008},
  pages = {337-340},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems, 14th International Conference, TACAS'08},
  publisher = {Springer},
  series = {LNCS},
  volume = {4963},
  documenturl = {http://research.microsoft.com/projects/z3/z3.pdf}
}

@inproceedings{Cadar:2008:KUA:1855741.1855756,
 author = {Cadar, Cristian and Dunbar, Daniel and Engler, Dawson},
 title = {KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs},
 booktitle = {Proc.\ 8th USENIX conference on Operating systems design and implementation},
 series = {OSDI'08},
 year = {2008},
 location = {San Diego, California},
 pages = {209--224},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=1855741.1855756},
 acmid = {1855756}
}

@article{Coen-Porisini:2001:USE:503271.503230,
 author = {Coen-Porisini, Alberto and Denaro, Giovanni and Ghezzi, Carlo and Pezz{\'e}, Mauro},
 title = {Using symbolic execution for verifying safety-critical systems},
 journal = {SIGSOFT Softw.\,Eng.\,Notes},
 issue_date = {Sept. 2001},
 volume = {26},
 number = {5},
 year = {2001},
 issn = {0163-5948},
 pages = {142--151},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/503271.503230},
 doi = {10.1145/503271.503230},
 acmid = {503230},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {formal methods, safety-critical system, symbolic execution, verification},
}

@inproceedings{Jaffar:2012:TSE:2362216.2362291,
 author = {Jaffar, Joxan and Murali, Vijayaraghavan and Navas, Jorge A. and Santosa, Andrew E.},
 title = {TRACER: a symbolic execution tool for verification},
 booktitle = {Proc.\ 24th international conference on Computer Aided Verification},
 series = {CAV'12},
 year = {2012},
 isbn = {978-3-642-31423-0},
 location = {Berkeley, CA},
 pages = {758--766},
 numpages = {9},
 url = {http://dx.doi.org/10.1007/978-3-642-31424-7_61},
 doi = {10.1007/978-3-642-31424-7_61},
 acmid = {2362291},
 publisher = {Springer-Verlag},
}

@inproceedings{Ramos:2011:PLE:2032305.2032360,
 author = {Ramos, David A and Engler, Dawson R.},
 title = {Practical, low-effort equivalence verification of real code},
 booktitle = {Proceedings of the 23rd international conference on Computer aided verification},
 series = {CAV'11},
 year = {2011},
 isbn = {978-3-642-22109-5},
 location = {Snowbird, UT},
 pages = {669--685},
 numpages = {17},
 url = {http://dl.acm.org/citation.cfm?id=2032305.2032360},
 acmid = {2032360},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{Clarke:2003:HVU:1119772.1119831,
 author = {Clarke, Edmund and Kroening, Daniel},
 title = {Hardware verification using ANSI-C programs as a reference},
 booktitle = {Proceedings of the 2003 Asia and South Pacific Design Automation Conference},
 series = {ASP-DAC '03},
 year = {2003},
 isbn = {0-7803-7660-9},
 location = {Kitakyushu, Japan},
 pages = {308--311},
 numpages = {4},
 url = {http://doi.acm.org/10.1145/1119772.1119831},
 doi = {10.1145/1119772.1119831},
 acmid = {1119831},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{Cui:2013:VSR:2499368.2451152,
 author = {Cui, Heming and Hu, Gang and Wu, Jingyue and Yang, Junfeng},
 title = {Verifying systems rules using rule-directed symbolic execution},
 journal = {SIGPLAN Not.},
 issue_date = {April 2013},
 volume = {48},
 number = {4},
 month = mar,
 year = {2013},
 issn = {0362-1340},
 pages = {329--342},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2499368.2451152},
 doi = {10.1145/2499368.2451152},
 acmid = {2451152},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {error detection, path slicing, symbolic execution, systems rules, verification},
}

@inproceedings{Barnett:2004:SPS:2131546.2131549,
 author = {Barnett, Mike and Leino, K. Rustan M. and Schulte, Wolfram},
 title = {The {Spec}\# programming system: an overview},
 booktitle = {Proc.\  2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices},
 series = {CASSIS'04},
 year = {2005},
 isbn = {3-540-24287-2, 978-3-540-24287-1},
 location = {Marseille, France},
 pages = {49--69},
 numpages = {21},
 url = {http://dx.doi.org/10.1007/978-3-540-30569-9_3},
 doi = {10.1007/978-3-540-30569-9_3},
 acmid = {2131549}
}

@article{KeY2005, 
  author        = {W. Ahrendt}, 
  title         = {The {KeY} Tool}, 
  journal       = {Software and Systems Modeling},   
  volume        = {4},
  pages         = {32-54},
  year          = {2005}, 
  doi           = {http://springerlink.metapress.com/openurl.asp?genre=article&id=doi:10.1007/s10270-004-0058-x},
  publisher     = {Springer}
}

@INPROCEEDINGS{Harel84dynamiclogic,
    author = {David Harel and Dexter Kozen and Jerzy Tiuryn},
    title = {Dynamic Logic},
    booktitle = {Handbook of Philosophical Logic},
    year = {1984},
    pages = {497--604},
    publisher = {MIT Press}
}

@inproceedings{Jacobs:2010:QTV:1947873.1947902,
 author = {Jacobs, Bart and Smans, Jan and Piessens, Frank},
 title = {A quick tour of the VeriFast program verifier},
 booktitle = {Proceedings of the 8th Asian conference on Programming languages and systems},
 series = {APLAS'10},
 year = {2010},
 isbn = {3-642-17163-X, 978-3-642-17163-5},
 location = {Shanghai, China},
 pages = {304--311},
 numpages = {8},
 url = {http://dl.acm.org/citation.cfm?id=1947873.1947902},
 acmid = {1947902},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@inproceedings{Reynolds:2002:SLL:645683.664578,
 author = {Reynolds, John C.},
 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
 booktitle = {Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science},
 series = {LICS '02},
 year = {2002},
 isbn = {0-7695-1483-9},
 pages = {55--74},
 numpages = {20},
 url = {http://dl.acm.org/citation.cfm?id=645683.664578},
 acmid = {664578},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}

@techreport{rosu-stefanescu-2011-tr, 
author = "Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu", 
institution={University of Illinois}, 
number={http://hdl.handle.net/2142/28357}, 
title = "Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework",
month = "November", 
year = "2011", 
}